A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)). f o g    A(C + Top) 

latex

ProofTree

Definitions	x:AB(x), t  T, x:A. B(x), S  T, Type, A, s = t, left + right, Top, f(a), P  Q, do-apply(f;x), b, , ff, can-apply(f;x), , b, x:A  B(x), P & Q, P  Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], p  q, p  q, p q, tt, , Unit, x.A(x), suptype(S; T), if b then t else f fi , Void, x:A.B(x), f o g  , False, inr x , Decision, True, inl x
Lemmas	true wf, false wf, ifthenelse wf, can-apply wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, do-apply wf, top wf, member wf